A:Realizer, i, x:Id, k:Knd, test:(State(R-state(A;i))Valtype(R-da(A;i);k)).
R-Feasible(A)
 x  dom(R-state(A;i))
 hasloc(k;i)
 write-restricted(A;i;k)
 (y:Id. y  dom(x :   R-state(A;i))  read-restricted(A; i; y))
 A || R-base-recognize(i;R-state(A;i);x;k;Valtype(R-da(A;i);k);test) 

latex

Definitions

Id, Type, R-state(R;i), IdDeq, f  g, R-da(R;i), Valtype(da;k), DeclaredType(ds;x), Top, f(x)?z, f(a), if b t else f fi, @loc effect knd(v:T)  x := f State(ds) v , A || B, x:A. B(x), , @loc only events in L change x:T, @loc x initially v:T, P & Q, Void, t  T, x:A. B(x), R-base-recognize(i;ds;x;k;T;test), P  Q, Realizer, Knd, x:AB(x), State(ds), R-Feasible(R), x. t(x), a:A fp B(a), x.A(x), x  dom(f), b, A, hasloc(k;i), write-restricted(R;i;k), read-restricted(R; i; y), x : v, false, type List, nil, car.cdr, KindDeq, isrcv(k), f || g, true, f  g, {T}, SQType(T), s = t, Prop, s ~ t, Atom$n, x:AB(x), P  Q

Lemmas

R-compat-self, assert-hasloc, Id sq, R-compat-da2, fpf-compatible-self, subtype rel self, fpf-compatible-single2, fpf-sub-join-right, ma-state-subtype, Reffect-compat, ifthenelse wf, btrue wf, fpf-cap-single-join, fpf-cap wf, isrcv wf, Kind-deq wf, Rframe-compat, Rinit-compat, bfalse wf, fpf-join wf, fpf-single wf, read-restricted wf, write-restricted wf, hasloc wf, not wf, assert wf, fpf-dom wf, id-deq wf, fpf-trivial-subtype-top, fpf wf, top wf, R-Feasible wf, decl-state wf, bool wf, Knd wf, Id wf, es realizer wf, R-compat-symmetry, R-base-recognize wf, R-state wf, ma-valtype wf, R-da wf, R-compat-Rplus-sq